(e sends on l with tag tg)
== e':es-E(es). ((es-kind(es; e') = rcv(l,tg)) c (es-sender(es; e') = e)) 

latex

---

clarification:

es-sends-on(es;e;l;tg)
== e':es-E(es). ((es-kind(es; e') = rcv(l,tg)  Knd) c (es-sender(es; e') = e  es-E(es))) 

latex

Definitions	x:A. B(x), A c B, Knd, es-kind(es; e), rcv(l,tg), s = t, es-E(es), es-sender(es; e)
FDL editor aliases	es-sends-on